p:FinProbSpace, n:, X, Y:RandomVariable(p;n).
E(n;(x.(x * x) * x) o X + Y)
=
((E(n;(x.(x * x) * x) o X) + (3 * E(n;X * X * Y)) + (3 * E(n;X * Y * Y)))
(+ E(n;(x.(x * x) * x) o Y))
  

latex

Definitions	t  T, True, (x.F(x)) o X, X + Y, <a, b>, RandomVariable(p;n), s = t, P  Q, False, A, A  B, , {x:A| B(x)} , , T, FinProbSpace, x:A. B(x), E(n;F), , r * s, x. t(x), x:AB(x), #$n, X * Y, q*X, P  Q, r + s, x:A  B(x), P & Q, P  Q, Outcome, {i..j}, Type, f(a), x.A(x)
Lemmas	qmul over plus qrng, qmul comm qrng, qmul ac 1 qrng, qmul assoc qrng, qadd ac 1 q, mon assoc q, qmul ident, q distrib, int seg wf, p-outcome wf, expectation-rv-scale, qadd wf, expectation-rv-add, rv-add wf, rv-scale wf, rv-mul wf, int inc rationals, rv-compose wf, qmul wf, rationals wf, expectation wf, squash wf, true wf, random-variable wf, nat wf, finite-prob-space wf